home *** CD-ROM | disk | FTP | other *** search
/ TeX 1995 July / TeX CD-ROM July 1995 (Disc 1)(Walnut Creek)(1995).ISO / macros / latex209 / contrib / misc / zed.sty < prev    next >
Text File  |  1993-01-11  |  10KB  |  324 lines
  1. %LaTeX style
  2. %
  3. % zed.sty 15 feb 88
  4. %
  5. \typeout{Style Option 'zed'. Released 15 February 1988}
  6.  
  7. %
  8. % Copyright (c) J.M. Spivey 1988
  9. %
  10. % This file contains a collection of macros for typesetting
  11. % Z specifications. There are four sections.
  12. %
  13. % 0. The mathcodes for letters are changed so that they generate text
  14. %    italic instead of math italic. This makes multi-letter identifiers
  15. %    look neater.
  16. %
  17. % 1. Environments for putting the maths in boxes.
  18. %
  19. % 2. Extra symbol fonts are loaded.
  20. %
  21. % 3. Mnemonics for Z symbols are defined. Note that certain plain TeX
  22. %    names are usurped here: \forall is made into a \mathop to give a
  23. %    thin space between it and the following declaration. The same goes
  24. %    for \lambda and \mu, and \exists.
  25. %
  26.  
  27. %
  28. % Changes since 25 aug 87
  29. %
  30. % 25 aug 87    Renamed \tad as \also and \also as \zbreak. \def'ed \tad
  31. %        to \also for upward compatibility.
  32. %        Inserted message on loading.
  33. %
  34. % 15 sep 87    Revamped special symbol names.
  35. %
  36. % 18 sep 87    Changed \z@d to allow Z text in lists. 
  37. %
  38. % 24 sep 87    Removed assignment to \prevdepth from \endschema
  39. %        --- giving a little more vertical space.
  40. %
  41. %  8 oct 87    Removed a spurious space from \schema --- caused
  42. %        empty paragraph between adjacent schemas.
  43. %        Merged left bar code into \axdef. Removed redef
  44. %        of \_.
  45. %
  46. % 12 oct 87    Removed \@zedwidth -- use \linewidth instead.
  47. %        Removed a spurious space from \z@dpream.
  48. %
  49. % 16 oct 87    Removed def of \par from \z@d.
  50. %
  51. % 10 dec 87    Removed spurious space from \gendef
  52. %
  53. % 15 jan 88    Split into two parts to allow both AMS and OXSY versions.
  54. %
  55. % 15 feb 88    Added gendef* environment
  56.  
  57. %
  58. % MATHCODES
  59. %
  60. % The mathcodes for the letters A, ..., Z, a, ..., z are changed to
  61. % generate text italic rather than math italic by default. This makes
  62. % multi-letter identifiers look better. The mathcode for character c
  63. % is set to "7000 (variable family) + "400 (text italic) + c.
  64. %
  65. % Also, the mathcode for semicolon is set to "8000, so it behaves as an
  66. % active character in math mode; it is defined to insert a thick space.
  67. % \semicolon is a semicolon as an ordinary symbol.
  68. %
  69.  
  70. \def\@setmcodes#1#2#3{{\count0=#1 \count1=#3
  71.     \loop \global\mathcode\count0=\count1 \ifnum \count0<#2
  72.     \advance\count0 by1 \advance\count1 by1 \repeat}}
  73.  
  74. \@setmcodes{`A}{`Z}{"7441}
  75. \@setmcodes{`a}{`z}{"7461}
  76.  
  77. \mathcode`\;="8000 % Makes ; active in math mode
  78. {\catcode`\;=\active \gdef;{\semicolon\;}}
  79. \mathchardef\semicolon="003B
  80.  
  81. %
  82. % SCHEMAS, Etc.
  83. %
  84. % Here are environments for the various sorts of
  85. % displays which occur in Z documents. All displays are set
  86. % flush left, indented by \zedindent, by default \leftmargini.
  87. % schemas, etc, are made just wide enough to give equal margins
  88. % left and right.
  89. %
  90. % Some environments (schema, etc.) must only be split at `\zbreak',
  91. % and others (argue) may be split arbitrarily. All generate alignment
  92. % displays, and penalties are used to control page breaks.
  93. %
  94. \newdimen\zedindent    \zedindent=\leftmargini
  95. \newdimen\zedleftsep    \zedleftsep=1em
  96. \newdimen\zedtab    \zedtab=2em
  97. \newdimen\zedbar    \zedbar=6em
  98. \newcount\interzedlinepenalty \interzedlinepenalty=10000
  99. \newcount\preboxpenalty \preboxpenalty=0
  100. \newif\ifzt@p        \zt@pfalse
  101.  
  102. \def\n@rrow{\advance\linewidth by-\zedindent}
  103. \def\t@pline#1{\omit \hbox to\linewidth{\strut
  104.     \leftt@p#1\thinspace\hrulefill}\cr}
  105. \def\z@dline{\omit \hbox to\linewidth{\hrulefill}\cr}
  106. \def\z@dpream{\halign to\linewidth\bgroup
  107.         \strut\z@dleft$\@lign##$\hfil \tabskip=0pt plus1fil%
  108.     &\hbox to0pt{\hss$\@lign##$}\tabskip=0pt\cr}
  109. \let\z@dleft=\relax
  110.  
  111. \def\zbreak{\crcr \noalign{\penalty\interdisplaylinepenalty} \also}
  112. \def\also{\crcr \noalign{\vskip\jot}}
  113. \def\tad{\also}
  114.  
  115. \def\@zed{\ifvmode\@zleavevmode\fi
  116.     $$\global\zt@ptrue \lineskip=0pt
  117.     \advance\linewidth by-\zedindent
  118.     \advance\displayindent by\zedindent
  119.     \def\\{\crcr}% Must have \def and not \let for nested alignments.
  120.     \everycr={\noalign{\ifzt@p \global\zt@pfalse
  121.         \else \penalty\interzedlinepenalty \fi}}
  122.         \tabskip=0pt}
  123. \def\end@zed{$$\global\@ignoretrue}
  124.  
  125. \def\zed{\@zed\z@dpream}
  126. \def\endzed{\crcr\egroup\end@zed}
  127.  
  128. \let\[=\zed
  129. \def\]{\crcr\egroup$$\ignorespaces}
  130.  
  131. \def\axdef{\let\zbreak=\zbre@k \let\also=\@lso \let\z@dleft=\@zedleft
  132.     \predisplaypenalty=\preboxpenalty \zed}
  133. \let\endaxdef=\endzed
  134. \def\zbre@k{\also \noalign{\penalty\interdisplaylinepenalty \vskip-\jot} \also}
  135. \def\@lso{\crcr \@but \omit\vrule height\jot \cr \@but}
  136. \def\@zedleft{\vrule\hskip\zedleftsep}
  137. \def\@but{\noalign{\nointerlineskip}}
  138.  
  139. \def\schema#1{\n@rrow\axdef \t@pline{$#1$}}
  140. \def\endschema{\also \z@dline \endzed}
  141.  
  142. \def\where{\also \omit \hbox to\zedbar{\hrulefill}\cr \also}
  143.  
  144. \@namedef{schema*}{\n@rrow\axdef
  145.     \noalign{\kern-\ht\strutbox} \z@dline \also}
  146. \expandafter\let\csname endschema*\endcsname=\endschema
  147.  
  148. \def\gendef#1{\let\leftt@p=\@leftt@p
  149.         \setbox0=\hbox{$[#1]$}\setbox1=\null \wd1=\wd0
  150.         \n@rrow\axdef \t@pline{\box0}%
  151.         \noalign{\kern-\baselineskip\kern-\doublerulesep \nobreak}%
  152.     \t@pline{\box1} \noalign{\kern\doublerulesep \nobreak}}
  153. \let\endgendef=\endschema
  154.  
  155. \@namedef{gendef*}{\n@rrow\axdef
  156.     \noalign{\kern-\ht\strutbox} \z@dline
  157.     \noalign{\kern-\baselineskip\kern-\doublerulesep \nobreak}
  158.     \z@dline \noalign{\kern\doublerulesep \nobreak} \also}
  159. \expandafter\let\csname endgendef*\endcsname=\endschema
  160.  
  161. % `infrule' environment: used for inference rules. The horizontal line is
  162. % generated by \derive: an optional argument contains the side-conditions
  163. % of the rule.
  164. \def\infrule{\@zed \halign\bgroup
  165.     \strut\quad$\@lign##$\quad\hfil&\quad\@lign##\hfil\cr}
  166. \let\endinfrule=\endzed
  167.  
  168. \def\derive{\crcr\also\@but\omit\hrulefill\@ifnextchar[{\@xderive}{\@yderive}}
  169. \def\@xderive[#1]{&$\smash{\lower 0.5ex\hbox{$[\;#1\;]$}}$\cr\also\@but}
  170. \def\@yderive{\cr\also\@but}
  171.  
  172. % `argue' environment: used for algebraic proofs expressed as extended
  173. % equations. Generates an alignment display, which may be split across
  174. % pages.
  175. \def\argue{\@zed \interzedlinepenalty=\interdisplaylinepenalty
  176.     \openup 1\jot \z@dpream \noalign{\vskip-\jot}}
  177. \let\endargue=\endzed
  178.  
  179. % `syntax' environment: used for syntax rules - even (once!) for VDM.
  180. \def\syntax{\@zed \halign\bgroup
  181.     \strut$\@lign##$\hfil &\hfil$\@lign{}##{}$\hfil
  182.     &$\@lign##$\hfil &\quad\@lign-- ##\hfil\cr}
  183. \let\endsyntax=\endzed
  184.  
  185. \def\@leftt@p{\vrule height0.4pt\hbox to\zedleftsep{\hrulefill\thinspace}}
  186. \let\leftt@p=\@leftt@p
  187. \def\leftschemas{\let\leftt@p=\relax}
  188.  
  189. \def\t#1{\hskip #1\zedtab}
  190. \def\flushr#1{\crcr\quad\cr}
  191.  
  192. % \@zleavevmode -- Enter horizontal mode, taking account of possible
  193. % interaction with lists and section heads:
  194. %    1    After a \item, use \indent to get the label (this
  195. %        fails to run in even short labels).
  196. %    2    After a run-in heading, use \indent.
  197. %    3    After an ordinary heading, throw away the \everypar
  198. %        tokens, reset \@nobreak, and use \noindent with \parskip
  199. %        zero.
  200. %    4    Otherwise, use \noindent with \parskip zero
  201. \def\@zleavevmode{\if@inlabel\indent\else\if@noskipsec\indent\else
  202.     \if@nobreak\global\@nobreakfalse\everypar={}\fi
  203.     {\parskip=0pt\noindent}\fi\fi}
  204.  
  205. %
  206. % FONTS
  207. %
  208. % The AMS extra symbol fonts are loaded.
  209. %
  210.  
  211. \def\@fontname{\ifcase\@ptsize m10 scaled \@m%
  212. \or m10 scaled \magstephalf%
  213. \or m10 scaled \magstep1%
  214. \else m\@ptsize\fi}
  215. \font\msx=msx\@fontname % Note: sometimes called euxm10
  216. \font\msy=msy\@fontname % Note: sometimes called euym10
  217.  
  218. \newfam\msxfam \textfont\msxfam=\msx
  219. \newfam\msyfam \textfont\msyfam=\msy
  220.  
  221. \def\@famletter#1{\ifcase #1 0\or 1\or 2\or 3\or 4\or 5\or 6\or 7\or
  222.     8\or 9\or A\or B\or C\or D\or E\or F\fi}
  223.  
  224. \edef\@fx{\@famletter\msxfam}
  225. \edef\@fy{\@famletter\msyfam}
  226.  
  227. \def\bbold{\fam\msyfam \msy}
  228.  
  229. %
  230. % Z SYMBOLS
  231. %
  232.  
  233. \def\token#1{\hbox{`$#1$'}} % makes a quoted expression in mathematical text
  234.  
  235. \def\report#1{\hbox{`{\tt #1}'}} % used for error messages in Z specs
  236.  
  237. % \@myop makes an operator, with a strut to defeat TeX's vertical adjustment.
  238. \def\@myop#1{\mathop{\mathstrut{#1}}\nolimits}
  239.  
  240. % This underscore doesn't have the little kern --- you get an italic
  241. % correction anyway in math mode.
  242. \def\_{\leavevmode \vbox{\hrule width0.5em}}
  243.  
  244. % Save \q as \xq for quantifiers q.
  245. \let\xforall=\forall
  246. \let\xexists=\exists
  247. \let\xlambda=\lambda
  248. \let\xmu=\mu
  249.  
  250. % \p and \f make arrows with 1 and 2 crossings resp.
  251. \def\p#1{\mathrel{\ooalign{\hfil$\mapstochar\mkern 5mu$\hfil\cr$#1$}}}
  252. \def\f#1{\mathrel{\ooalign{\hfil
  253.     $\mapstochar\mkern 3mu\mapstochar\mkern 5mu$\hfil\cr$#1$}}}
  254.  
  255. \let\@mc=\mathchardef
  256.  
  257. % In the same order as the Z reference manual ...
  258.  
  259. % Chapter 1
  260. \def \lblot    {\langle\!\left|}
  261. \def \rblot    {\right|\!\rangle}
  262.  
  263. % Chapter 2
  264. \def \defs    {\mathrel{\widehat=}}
  265. \def \power    {\@myop{\bbold P}}
  266. \let \cross    \times
  267. \def \lambda    {\@myop{\xlambda}}
  268. \def \mu    {\@myop{\xmu}}
  269. \def \lbag    {[\![}
  270. \def \rbag    {]\!]}
  271. \def \lnot    {\neg\;}
  272. \def \land    {\mathrel{\wedge}}
  273. \def \lor    {\mathrel{\vee}}
  274. \let \implies    \Rightarrow
  275. \let \iff    \Leftrightarrow
  276. \def \forall    {\@myop{\xforall}}
  277. \def \exists    {\@myop{\xexists}}
  278. \def \spot    {\mathrel{\bullet}}
  279. \def \hide    {\mathrel{\backslash}}
  280. \@mc \project    "3\@fx16
  281. \def \pre    {\@myop{\rm pre}}
  282. \def \semi    {\mathrel{\comp}}
  283. \def \ldata    {\langle\!\langle}
  284. \def \rdata    {\rangle\!\rangle}
  285. \def \shows    {\;\vdash\;}
  286.  
  287. % Chapter 3
  288. \@mc \empty    "0\@fy3F
  289. \let \rel    \leftrightarrow
  290. \def \dom    {\@myop{\rm dom}}
  291. \def \ran    {\@myop{\rm ran}}
  292. \def \id    {\@myop{\rm id}}
  293. \def \comp    {\mathbin{\raise 0.6ex\hbox{\oalign{\hfil$\scriptscriptstyle
  294.          \rm o$\hfil\cr\hfil$\scriptscriptstyle\rm 9$\hfil}}}}
  295. \@mc \dres    "2\@fx43
  296. \@mc \rres    "2\@fx42
  297. \def \ndres    {\mathbin{\rlap{$-$}{\dres}}}
  298. \def \nrres    {\mathbin{\rlap{$-$}{\rres}}}
  299. \def \limg    {(\!\left|}
  300. \def \rimg    {\right|\!)}
  301. \def \pfun    {\p\fun}
  302. \let \fun    \rightarrow
  303. \def \pinj    {\p\inj}
  304. \@mc \inj    "3\@fx1A
  305. \def \psurj    {\p\surj}
  306. \def \surj    {\mathrel{\ooalign{$\fun$\hfil\cr$\mkern4mu\fun$}}}
  307. \def \bij    {\mathrel{\ooalign{$\inj$\hfil\cr$\mkern5mu\fun$}}}
  308. \def \nat    {{\bbold N}}
  309. \def \num    {{\bbold Z}}
  310. \def \div    {\mathbin{\rm div}}
  311. \def \mod    {\mathbin{\rm mod}}
  312. \def \upto    {\mathbin{\ldotp\ldotp}}
  313. \def \finset    {\@myop{\bbold F}}
  314. \def \ffun    {\f\fun}
  315. \def \finj    {\f\inj}
  316. \def \seq    {\@myop{\rm seq}}
  317. \def \cat    {\mathbin{\raise 0.8ex\hbox{$\mathchar"2\@fx61$}}}
  318. \@mc \filter    "2\@fx16
  319. \def \dcat    {\@myop{\cat/}}
  320. \def \disjoint  {{\rm disjoint}\;}
  321. \def \partition {\mathrel{\rm partition}}
  322. \def \bag    {\@myop{\rm bag}}
  323. \def \inbag     {\mathrel{\rm in}}
  324.